The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(1, n^1).

0 CpxRelTRS
↳1 RelTrsToTrsProof (UPPER BOUND(ID), 0 ms)
↳2 CpxTRS
↳3 CpxTrsToCdtProof (BOTH BOUNDS(ID, ID), 7 ms)
↳4 CdtProblem
↳5 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID), 0 ms)
↳6 CdtProblem
↳7 CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID), 0 ms)
↳8 CdtProblem
↳9 CdtGraphSplitRhsProof (BOTH BOUNDS(ID, ID), 0 ms)
↳10 CdtProblem
↳11 CdtLeafRemovalProof (ComplexityIfPolyImplication, 0 ms)
↳12 CdtProblem
↳13 CdtUsableRulesProof (⇔, 0 ms)
↳14 CdtProblem
↳15 CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)), 49 ms)
↳16 CdtProblem
↳17 SIsEmptyProof (BOTH BOUNDS(ID, ID), 0 ms)
↳18 BOUNDS(1, 1)

(0) Obligation:

The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(1, n^1).


The TRS R consists of the following rules:

lte(Cons(x', xs'), Cons(x, xs)) → lte(xs', xs)
lte(Cons(x, xs), Nil) → False
even(Cons(x, Nil)) → False
even(Cons(x', Cons(x, xs))) → even(xs)
notEmpty(Cons(x, xs)) → True
notEmpty(Nil) → False
lte(Nil, y) → True
even(Nil) → True
goal(x, y) → and(lte(x, y), even(x))

The (relative) TRS S consists of the following rules:

and(False, False) → False
and(True, False) → False
and(False, True) → False
and(True, True) → True

Rewrite Strategy: INNERMOST

(1) RelTrsToTrsProof (UPPER BOUND(ID) transformation)

transformed relative TRS to TRS

(2) Obligation:

The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(1, n^1).


The TRS R consists of the following rules:

lte(Cons(x', xs'), Cons(x, xs)) → lte(xs', xs)
lte(Cons(x, xs), Nil) → False
even(Cons(x, Nil)) → False
even(Cons(x', Cons(x, xs))) → even(xs)
notEmpty(Cons(x, xs)) → True
notEmpty(Nil) → False
lte(Nil, y) → True
even(Nil) → True
goal(x, y) → and(lte(x, y), even(x))
and(False, False) → False
and(True, False) → False
and(False, True) → False
and(True, True) → True

Rewrite Strategy: INNERMOST

(3) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID) transformation)

Converted Cpx (relative) TRS to CDT

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

lte(Cons(z0, z1), Cons(z2, z3)) → lte(z1, z3)
lte(Cons(z0, z1), Nil) → False
lte(Nil, z0) → True
even(Cons(z0, Nil)) → False
even(Cons(z0, Cons(z1, z2))) → even(z2)
even(Nil) → True
notEmpty(Cons(z0, z1)) → True
notEmpty(Nil) → False
goal(z0, z1) → and(lte(z0, z1), even(z0))
and(False, False) → False
and(True, False) → False
and(False, True) → False
and(True, True) → True
Tuples:

LTE(Cons(z0, z1), Cons(z2, z3)) → c(LTE(z1, z3))
LTE(Cons(z0, z1), Nil) → c1
LTE(Nil, z0) → c2
EVEN(Cons(z0, Nil)) → c3
EVEN(Cons(z0, Cons(z1, z2))) → c4(EVEN(z2))
EVEN(Nil) → c5
NOTEMPTY(Cons(z0, z1)) → c6
NOTEMPTY(Nil) → c7
GOAL(z0, z1) → c8(AND(lte(z0, z1), even(z0)), LTE(z0, z1), EVEN(z0))
AND(False, False) → c9
AND(True, False) → c10
AND(False, True) → c11
AND(True, True) → c12
S tuples:

LTE(Cons(z0, z1), Cons(z2, z3)) → c(LTE(z1, z3))
LTE(Cons(z0, z1), Nil) → c1
LTE(Nil, z0) → c2
EVEN(Cons(z0, Nil)) → c3
EVEN(Cons(z0, Cons(z1, z2))) → c4(EVEN(z2))
EVEN(Nil) → c5
NOTEMPTY(Cons(z0, z1)) → c6
NOTEMPTY(Nil) → c7
GOAL(z0, z1) → c8(AND(lte(z0, z1), even(z0)), LTE(z0, z1), EVEN(z0))
AND(False, False) → c9
AND(True, False) → c10
AND(False, True) → c11
AND(True, True) → c12
K tuples:none
Defined Rule Symbols:

lte, even, notEmpty, goal, and

Defined Pair Symbols:

LTE, EVEN, NOTEMPTY, GOAL, AND

Compound Symbols:

c, c1, c2, c3, c4, c5, c6, c7, c8, c9, c10, c11, c12

(5) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)

Removed 10 trailing nodes:

EVEN(Nil) → c5
NOTEMPTY(Cons(z0, z1)) → c6
AND(True, True) → c12
AND(False, True) → c11
AND(False, False) → c9
NOTEMPTY(Nil) → c7
EVEN(Cons(z0, Nil)) → c3
LTE(Cons(z0, z1), Nil) → c1
LTE(Nil, z0) → c2
AND(True, False) → c10

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

lte(Cons(z0, z1), Cons(z2, z3)) → lte(z1, z3)
lte(Cons(z0, z1), Nil) → False
lte(Nil, z0) → True
even(Cons(z0, Nil)) → False
even(Cons(z0, Cons(z1, z2))) → even(z2)
even(Nil) → True
notEmpty(Cons(z0, z1)) → True
notEmpty(Nil) → False
goal(z0, z1) → and(lte(z0, z1), even(z0))
and(False, False) → False
and(True, False) → False
and(False, True) → False
and(True, True) → True
Tuples:

LTE(Cons(z0, z1), Cons(z2, z3)) → c(LTE(z1, z3))
EVEN(Cons(z0, Cons(z1, z2))) → c4(EVEN(z2))
GOAL(z0, z1) → c8(AND(lte(z0, z1), even(z0)), LTE(z0, z1), EVEN(z0))
S tuples:

LTE(Cons(z0, z1), Cons(z2, z3)) → c(LTE(z1, z3))
EVEN(Cons(z0, Cons(z1, z2))) → c4(EVEN(z2))
GOAL(z0, z1) → c8(AND(lte(z0, z1), even(z0)), LTE(z0, z1), EVEN(z0))
K tuples:none
Defined Rule Symbols:

lte, even, notEmpty, goal, and

Defined Pair Symbols:

LTE, EVEN, GOAL

Compound Symbols:

c, c4, c8

(7) CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID) transformation)

Removed 1 trailing tuple parts

(8) Obligation:

Complexity Dependency Tuples Problem
Rules:

lte(Cons(z0, z1), Cons(z2, z3)) → lte(z1, z3)
lte(Cons(z0, z1), Nil) → False
lte(Nil, z0) → True
even(Cons(z0, Nil)) → False
even(Cons(z0, Cons(z1, z2))) → even(z2)
even(Nil) → True
notEmpty(Cons(z0, z1)) → True
notEmpty(Nil) → False
goal(z0, z1) → and(lte(z0, z1), even(z0))
and(False, False) → False
and(True, False) → False
and(False, True) → False
and(True, True) → True
Tuples:

LTE(Cons(z0, z1), Cons(z2, z3)) → c(LTE(z1, z3))
EVEN(Cons(z0, Cons(z1, z2))) → c4(EVEN(z2))
GOAL(z0, z1) → c8(LTE(z0, z1), EVEN(z0))
S tuples:

LTE(Cons(z0, z1), Cons(z2, z3)) → c(LTE(z1, z3))
EVEN(Cons(z0, Cons(z1, z2))) → c4(EVEN(z2))
GOAL(z0, z1) → c8(LTE(z0, z1), EVEN(z0))
K tuples:none
Defined Rule Symbols:

lte, even, notEmpty, goal, and

Defined Pair Symbols:

LTE, EVEN, GOAL

Compound Symbols:

c, c4, c8

(9) CdtGraphSplitRhsProof (BOTH BOUNDS(ID, ID) transformation)

Split RHS of tuples not part of any SCC

(10) Obligation:

Complexity Dependency Tuples Problem
Rules:

lte(Cons(z0, z1), Cons(z2, z3)) → lte(z1, z3)
lte(Cons(z0, z1), Nil) → False
lte(Nil, z0) → True
even(Cons(z0, Nil)) → False
even(Cons(z0, Cons(z1, z2))) → even(z2)
even(Nil) → True
notEmpty(Cons(z0, z1)) → True
notEmpty(Nil) → False
goal(z0, z1) → and(lte(z0, z1), even(z0))
and(False, False) → False
and(True, False) → False
and(False, True) → False
and(True, True) → True
Tuples:

LTE(Cons(z0, z1), Cons(z2, z3)) → c(LTE(z1, z3))
EVEN(Cons(z0, Cons(z1, z2))) → c4(EVEN(z2))
GOAL(z0, z1) → c1(LTE(z0, z1))
GOAL(z0, z1) → c1(EVEN(z0))
S tuples:

LTE(Cons(z0, z1), Cons(z2, z3)) → c(LTE(z1, z3))
EVEN(Cons(z0, Cons(z1, z2))) → c4(EVEN(z2))
GOAL(z0, z1) → c1(LTE(z0, z1))
GOAL(z0, z1) → c1(EVEN(z0))
K tuples:none
Defined Rule Symbols:

lte, even, notEmpty, goal, and

Defined Pair Symbols:

LTE, EVEN, GOAL

Compound Symbols:

c, c4, c1

(11) CdtLeafRemovalProof (ComplexityIfPolyImplication transformation)

Removed 2 leading nodes:

GOAL(z0, z1) → c1(LTE(z0, z1))
GOAL(z0, z1) → c1(EVEN(z0))

(12) Obligation:

Complexity Dependency Tuples Problem
Rules:

lte(Cons(z0, z1), Cons(z2, z3)) → lte(z1, z3)
lte(Cons(z0, z1), Nil) → False
lte(Nil, z0) → True
even(Cons(z0, Nil)) → False
even(Cons(z0, Cons(z1, z2))) → even(z2)
even(Nil) → True
notEmpty(Cons(z0, z1)) → True
notEmpty(Nil) → False
goal(z0, z1) → and(lte(z0, z1), even(z0))
and(False, False) → False
and(True, False) → False
and(False, True) → False
and(True, True) → True
Tuples:

LTE(Cons(z0, z1), Cons(z2, z3)) → c(LTE(z1, z3))
EVEN(Cons(z0, Cons(z1, z2))) → c4(EVEN(z2))
S tuples:

LTE(Cons(z0, z1), Cons(z2, z3)) → c(LTE(z1, z3))
EVEN(Cons(z0, Cons(z1, z2))) → c4(EVEN(z2))
K tuples:none
Defined Rule Symbols:

lte, even, notEmpty, goal, and

Defined Pair Symbols:

LTE, EVEN

Compound Symbols:

c, c4

(13) CdtUsableRulesProof (EQUIVALENT transformation)

The following rules are not usable and were removed:

lte(Cons(z0, z1), Cons(z2, z3)) → lte(z1, z3)
lte(Cons(z0, z1), Nil) → False
lte(Nil, z0) → True
even(Cons(z0, Nil)) → False
even(Cons(z0, Cons(z1, z2))) → even(z2)
even(Nil) → True
notEmpty(Cons(z0, z1)) → True
notEmpty(Nil) → False
goal(z0, z1) → and(lte(z0, z1), even(z0))
and(False, False) → False
and(True, False) → False
and(False, True) → False
and(True, True) → True

(14) Obligation:

Complexity Dependency Tuples Problem
Rules:none
Tuples:

LTE(Cons(z0, z1), Cons(z2, z3)) → c(LTE(z1, z3))
EVEN(Cons(z0, Cons(z1, z2))) → c4(EVEN(z2))
S tuples:

LTE(Cons(z0, z1), Cons(z2, z3)) → c(LTE(z1, z3))
EVEN(Cons(z0, Cons(z1, z2))) → c4(EVEN(z2))
K tuples:none
Defined Rule Symbols:none

Defined Pair Symbols:

LTE, EVEN

Compound Symbols:

c, c4

(15) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

LTE(Cons(z0, z1), Cons(z2, z3)) → c(LTE(z1, z3))
EVEN(Cons(z0, Cons(z1, z2))) → c4(EVEN(z2))
We considered the (Usable) Rules:none
And the Tuples:

LTE(Cons(z0, z1), Cons(z2, z3)) → c(LTE(z1, z3))
EVEN(Cons(z0, Cons(z1, z2))) → c4(EVEN(z2))
The order we found is given by the following interpretation:
Polynomial interpretation :

POL(Cons(x1, x2)) = [2] + x2   
POL(EVEN(x1)) = [2]x1   
POL(LTE(x1, x2)) = x2   
POL(c(x1)) = x1   
POL(c4(x1)) = x1   

(16) Obligation:

Complexity Dependency Tuples Problem
Rules:none
Tuples:

LTE(Cons(z0, z1), Cons(z2, z3)) → c(LTE(z1, z3))
EVEN(Cons(z0, Cons(z1, z2))) → c4(EVEN(z2))
S tuples:none
K tuples:

LTE(Cons(z0, z1), Cons(z2, z3)) → c(LTE(z1, z3))
EVEN(Cons(z0, Cons(z1, z2))) → c4(EVEN(z2))
Defined Rule Symbols:none

Defined Pair Symbols:

LTE, EVEN

Compound Symbols:

c, c4

(17) SIsEmptyProof (BOTH BOUNDS(ID, ID) transformation)

The set S is empty

(18) BOUNDS(1, 1)